""" This module contains the definitions of the dynamic part of pi-graphs
"""
from name import LocalName, Guard, Mismatch, InputName, OutputName, BOTTOM, Name, \
    FreshName, NameComparison
from pi.action import AtomicRewrite, StrlType, Input, Output, SyncRewrite, \
    Silence
from pi.name import PrivateName, Match, FreeName

class TupleMap:
    """ List (tuple) of tuples
    This is the basic data structure for the context
    """
    def __init__(self, src=None):
        """
        @param src: data used for constructing a TupleMap
        """
        if src is None:
            data = tuple()
        elif isinstance(src, list):
            data = tuple(src)
        elif isinstance(src, tuple):
            data = src
        elif isinstance(src, TupleMap):
            data = src.map()
        self._data = data
        
    def map(self, n=None):
        """ Get one/all tuples
        """
        if n is None:
            return self._data
        else:
            return self._data[n]
               
    def pos(self, k, v=None):
        """ Find the position of a tuple
        @param k: first element of the tuple
        @param v: second element of the tuple
        @return: position, -1 if not found
        """
        l = 0
        r = len(self._data) - 1
        if v is None:
            while l <= r:
                m = (l + r) / 2
                if self._data[m][0] == k:
                    return m
                elif self._data[m][0] < k:
                    l = m + 1
                else:
                    r = m - 1
        else:
            t = (k, v)
            while l <= r:
                m = (l + r) / 2
                if self._data[m] == t:
                    return m
                elif self._data[m] < t:
                    l = m + 1
                else:
                    r = m - 1
        return -1
    
    def hole(self, k, v):
        """ Find the position p for inserting on the LEFT
            all tuples from position p are shift right
        @param (k,v): the inserted tuple
        @return: the position 
        """
        if len(self._data) == 0:
            return 0
        t = (k, v)
        l = 0
        r = len(self._data) - 1
        while l <= r:
            m = (l + r) / 2
            if self._data[m] == t:
                return m
            elif self._data[m] < t:
                l = m + 1
            else:
                r = m - 1
        if self._data[m] < t:
            return m + 1
        else:
            return m
        
    def has(self, k, v=None):
        """ Check if there exists a tuple
        """
        p = self.pos(k, v)
        return p != -1
        
    def insert(self, k, v):
        """ Insert a tuple
        """
        h = self.hole(k, v)
        M = self._data[:h] + ((k, v),) + self._data[h:]
        return TupleMap(M)
    
    def remove(self, K, v=None):
        """ Remove tuples
        @param K: set of first elements of tuples are removed (if v is omitted)
            if v is present, remove a tuple (K,v)
        @return: A TupleMap after removing
        """
        M = self._data
        if v is None:
            for k in K:
                l = 0
                r = len(M) - 1
                while l <= r:
                    m = (l + r) / 2
                    if M[m][0] == k:
                        break
                    elif M[m][0] < k:
                        l = m + 1
                    else:
                        r = m - 1
                if l > r:  # not found
                    continue
                l = r = m
                while l >= 0 and M[l][0] == k:
                    l = l - 1
                while r < len(M) and M[r][0] == k:
                    r = r + 1
                M = M[:l + 1] + M[r:]
        elif self.has(K, v):
            l = r = self.pos(K, v)
            while l >= 0 and M[l] == (K, v):
                l = l - 1
            while r < len(M) and M[r] == (K, v):
                r = r + 1
            M = M[:l + 1] + M[r:]
        return TupleMap(M)
    
    def replace(self, k, v):
        """ Replace the value of a given key by another value
        @requires: k is unique
        @return: A TupleMap after replacing
        """
        p = self.pos(k)
        M = self._data[:p] + ((k, v),) + self._data[p + 1:]
        return TupleMap(M)

    def dom(self):
        """ Get the domain of the map (set of keys)
        """
        return set(map(lambda t: t[0], self._data))
    
    def cod(self):
        """ Get the co-domain of the map (set of values)
        """
        return set(map(lambda t: t[1], self._data))
    
    def val(self, k):
        """ Get the value of a given key
        @requires: the key must be existed
        @return: the value
        """
        p = self.pos(k)
        if p == -1:
            raise KeyError()
        return self._data[p][1]
    
    def __hash__(self):
        return hash(self._data)
    
    def __eq__(self, other):
        if not isinstance(other, TupleMap):
            return False
        return self._data == other.map()
    
    def __ne__(self, other):  # TODO: should use hash value
        if not isinstance(other, TupleMap):
            return True
        return self._data != other.map()
    
    def __gt__(self, other):
        if not isinstance(other, TupleMap):
            return False
        return self._data > other.map()

    def __ge__(self, other):
        if not isinstance(other, TupleMap):
            return False
        return self._data >= other.map()

    def __lt__(self, other):
        if not isinstance(other, TupleMap):
            return False
        return self._data < other.map()
    
    def __le__(self, other):
        if not isinstance(other, TupleMap):
            return False
        return self._data <= other.map()
    
    def __len__(self):
        return len(self._data)
    
    def __str__(self):
        s = ", ".join("%s:%s" % (t[0], t[1]) for t in self._data)
        return "{%s}" % s
    
    def __repr__(self):
        s = ", ".join("%r:%r" % (t[0], t[1]) for t in self._data)
        return "{%s}" % s


class NameEnv(TupleMap):
    """ A map from names to their instances.
    """
    def __init__(self, src):
        TupleMap.__init__(self, src)
               
    def hasName(self, name):
        """ Check if there exist a given name be used
        """
        found = False
        for t in self._data:
            if t[0] == name or t[1] == name:
                found = True
                break
        return found


class Partitions(TupleMap):
    """ The dynamic partitions 
    """
    def __init__(self, src):
        TupleMap.__init__(self, src)
        
    def removeName(self, names):
        """ Remove names from dynamic partitions
        """
        if isinstance(names, Name):
            names = [names]
        return Partitions(self.remove(names))
    
    def addName(self, name, p):
        """ Add a name to a given partition
        @requires: name does not exist
        """
        if self.has(name):
            raise Exception("name existed")
        return Partitions(self.insert(name, p))
        
    def hasPartition(self, p):
        """ Test if there exist a partition with given ID
        """
        return p in self.cod()
    
    def newPartition(self):
        """ Compute the ID of next partition
        """
        k = 1
        while k in self.cod():
            k = k + 1
        return k
    
    def join(self, p1, p2):
        """ Join two partitions
        """
        if p1 > p2: p1, p2 = p2, p1
        M = []
        for t in self._data:
            if t[1] == p2:
                M.append((t[0], p1))
            else:
                M.append(t)
        return Partitions(M)
    
    def computeMap(self):
        """ Compute a mapping of index
            in which the index are minimum and continuous
        """
        if len(self._data) == 0:
            return None
        M = {}
        i = 0
        P = map(lambda t: t[1], self._data)
        for p in P:
            if not M.has_key(p):
                i = i + 1
                M[p] = i
        new = False
        for p, i in M.items():
            if p != i:
                new = True
                break
        if new:
            return M
        else:
            return None
    
    def reindex(self, M):
        """ Applying a mapping of index
        """
        P = []
        for t in self._data:
            P.append((t[0], M[t[1]]))
        return Partitions(P)
    

class Distinctions(TupleMap):
    """ A distinction
    """   
    def __init__(self, src):
        TupleMap.__init__(self, src)
        
    def distinct(self, p1, p2):
        """ Check if there exists a distinction
        """
        if p1 == p2:
            return False
        if p1 > p2: 
            p1, p2 = p2, p1
        return self.has(p1, p2)
        
    def addDistinction(self, p1, p2):
        """ Add a distinction
        """
        if isinstance(p2, int):
            if p1 > p2: 
                p1, p2 = p2, p1
            return Distinctions(self.insert(p1, p2))
        else:
            E = []
            for e in self._data:
                E.append(e)
            for p in p2:
                if p == p1:
                    break
                if p1 < p:
                    E.append((p1, p))
                else:
                    E.append((p, p1))
            E.sort()
            return Distinctions(E)
    
    def join(self, p1, p2):
        """ Join two partitions
        """
        if p1 > p2:
            p1, p2 = p2, p1
        E = []
        for e in self._data:
            if e[0] != p2 and e[1] != p2:
                E.append(e)
            elif e[0] == p2 and not self.distinct(p1, e[1]):
                a, b = p1, e[1]
                if a > b: a, b = b, a
                E.append((a, b))
            elif e[1] == p2 and not self.distinct(p1, e[0]):
                a, b = p1, e[0]
                if a > b: a, b = b, a
                E.append((a, b))
        E.sort()
        return Distinctions(E)
    
    def removePartition(self, P):
        ''' Remove all distinctions to given partitions.'''
        # remove in the domain
        E = self.remove(P).map()
        # remove in the co-domain
        if isinstance(P, int):
            P = [P]
        for p in P:
            k = 0
            while k != -1:
                k = -1
                for i in range(len(E)):
                    if E[i][1] == p:
                        k = i
                        break
                if k != -1:
                    E = E[:k] + E[k + 1:]
        return Distinctions(E)
    
    def reindex(self, M):
        """ Apply a new mapping
        """
        if M is None:
            return self
        E = []
        for e in self._data:
            p1 = M[e[0]]
            p2 = M[e[1]]
            if p1 > p2: 
                p1, p2 = p2, p1
            E.append((p1, p2))
        E.sort()
        return Distinctions(E)
    
    def __str__(self):
        s = ", ".join("%d<->%d" % (e[0], e[1]) for e in self._data)
        return "{%s}" % s

    def __repr__(self):
        s = ", ".join("%d<->%d" % (e[0], e[1]) for e in self._data)
        return "{%s}" % s
    

class NameContext:
    """ A name context
    """
    def __init__(self, namenv, partitions, distinctions):
            self._namenv = namenv
            self._parts = partitions
            self._dists = distinctions
        
    def namenv(self):
        """ Get the name environment component
        """
        return self._namenv
    
    def partitions(self):
        """ Get the partitions component
        """
        return self._parts
    
    def distinctions(self):
        """ Get the distinctions component
        """
        return self._dists
        
    def fresh(self, name):
        """ Check if a name is fresh
        """
        if name is BOTTOM:
            return False
        return not self._namenv.hasName(name)
    
    def instance(self, name, i=None):
        """ Get instance of a name
        """
        if isinstance(name, LocalName) and i is not None:
            name = name.setThread(i)
        p = self._namenv.pos(name)
        if p == -1:
            raise NameError("name not found")
        return self._namenv.map()[p][1]
    
    def removeInstance(self, names, i=None):
        """ Remove instances of a set of names
        """
        N = names
        if isinstance(names, Name):
            N = [names]
        # Update the name environment
        L = set()
        R = set()
        for name in N:
            fname = name
            if isinstance(name, LocalName) and i is not None:
                fname = name.setThread(i)
            L.add(fname)
            R.add(self.instance(fname))
        new_namenv = NameEnv(self._namenv.remove(L))
        # Update the partitions
        N = R
        L = set()  # removed names in domain
        IDs = set()  # removed partitions
        for name in N:
            if name is not BOTTOM and not new_namenv.hasName(name):  # unused names
                L.add(name)
                IDs.add(self._parts.val(name))
        new_parts = Partitions(self._parts.remove(L))
        # Update distinctions
        X = set()
        for ID in IDs:
            if not new_parts.hasPartition(ID):
                X.add(ID)
        new_dists = self._dists.removePartition(X)
        # New name-context
        return NameContext(new_namenv, new_parts, new_dists)
    
    def insertInstance(self, name, instance, i):
        """ Insert an instance of a given name
        """
        E = self._namenv
        P = self._parts
        D = self._dists
        # Create new name environment
        if isinstance(name, LocalName):
            name = name.setThread(i)
        E = NameEnv(E.insert(name, instance))
        # Update partitions and distinctions if instance is fresh
        if self.fresh(instance):
            k = P.newPartition()
            P = P.addName(instance, k)
            if isinstance(instance, PrivateName):
                D = D.addDistinction(k, P.cod())
            else:  # instance is not a private name
                IDs = set()
                for name in P.dom():
                    if isinstance(name, PrivateName):
                        IDs.add(P.val(name))
                D = D.addDistinction(k, IDs)
        return NameContext(E, P, D)
    
    def instantiate(self, name, instance, i):
        """ Instantiate a name
        """
        nnc = self.removeInstance(name, i)
        nnc = nnc.insertInstance(name, instance, i)
        return nnc
    
    def exchange(self, priv_name, outname):
        """ Do exchange a private name by fresh output-name
        """
        # Create new name environment
        xnames = []  # Names that there instance will be changed
        for name in self._namenv.dom():
            if self._namenv.val(name) == priv_name:
                xnames.append(name)
        E = self._namenv.remove(xnames)
        for name in xnames:
            E = E.insert(name, outname)
        # Create new partitions
        k = self._parts.val(priv_name)
        P = self._parts.removeName(priv_name)
        P = P.addName(outname, k)
        # Create new distinctions
        D = self._dists.removePartition([k])
        fresh_IDs = set()  # IDs of fresh-names
        for name in self._parts.dom():
            if isinstance(name, FreshName):
                fresh_IDs.add(self._parts.val(name))
        D = D.addDistinction(k, fresh_IDs)
        return NameContext(NameEnv(E), P, D)
    
    def refine(self, c):
        """ Refine a match/mismatch
        """
        p1 = self._parts.val(c.firstname())
        p2 = self._parts.val(c.secondname())
        if isinstance(c, Match) and p1 != p2:
            P = self._parts.join(p1, p2)
            D = self._dists.join(p1, p2)
            return NameContext(self._namenv, P, D)
        elif isinstance(c, Mismatch) and not self._dists.distinct(p1, p2):
            D = self._dists.addDistinction(p1, p2)
            return NameContext(self._namenv, self._parts, D)
        else:
            return self
    
    def substitute(self, guard, i):
        """ Do substitute a guard and return new one
        """
        C = []
        for c in guard.comparison():
            n1 = self.instance(c.firstname(), i)
            n2 = self.instance(c.secondname(), i)
            if isinstance(c, Match):
                C.append(Match(n1, n2))
            else:
                C.append(Mismatch(n1, n2))
        return Guard(C)
    
    def check(self, C):
        """ Check if a guard can be applied
        """
        if isinstance(C, NameComparison):
            p1 = self._parts.val(C.firstname())
            p2 = self._parts.val(C.secondname())
            if isinstance(C, Mismatch):
                return p1 != p2
            else:
                return (p1 == p2 or not self._dists.distinct(p1, p2))
        else:
            nnc = self
            for i in range(len(C)):
                if not nnc.check(C[i]):
                    return False
                nnc = nnc.refine(C[i])
            return True
    
    def eval(self, guard):
        """ Do evaluate a guard and return new context
        """
        nnc = self
        for i in range(len(guard)):
            nnc = nnc.refine(guard[i])
        return nnc
        
    def nextInputName(self):
        ''' Get next input name.'''
        IDs = set()
        for name in self._namenv.cod():
            if isinstance(name, InputName):
                IDs.add(name.getID())
        k = 1
        while k in IDs:
            k = k + 1
        return InputName(k)
    
    def nextOutputName(self):
        ''' Get next output name.'''
        IDs = set()
        for name in self._namenv.cod():
            if isinstance(name, OutputName):
                IDs.add(name.getID())
        k = 1
        while k in IDs:
            k = k + 1
        return OutputName(k)
    
    def nextPrivateName(self):
        ''' Get next private name.'''
        IDs = set()
        for name in self._namenv.cod():
            if isinstance(name, PrivateName):
                IDs.add(name.getID())
        k = 1
        while k in IDs:
            k = k + 1
        return PrivateName(k)
    
    def init(self, rname, i, grp):
        """ Initialize local names
        """
        varnames = grp.replicator(rname).varNames()
        tresnames = grp.replicator(rname).tresNames()
        nnc = self
        for name in varnames:
            nnc = nnc.insertInstance(name, BOTTOM, i)
        for name in tresnames:
            privname = nnc.nextPrivateName()
            nnc = nnc.insertInstance(name, privname, i)
        return nnc
    
    def reset(self, rname, i):
        """ Reset local names of a thread.
        """
        xnames = []
        for name in self._namenv.dom():
            if isinstance(name, LocalName):
                if name.rname() == rname and name.thread() == i:
                    xnames.append(name)        
        return self.removeInstance(xnames)
    
    def normalize(self):
        m = self._parts.computeMap()
        if m is None:
            return self
        P = self._parts.reindex(m)
        D = self._dists.reindex(m)
        return NameContext(self._namenv, P, D)
    
    def compare(self, other):
        """Comparison vector
        """
        if self._namenv < other.namenv():
            n = -1
        elif self._namenv > other.namenv():
            n = 1
        else: n = 0
        #
        if self._parts < other.partitions():
            p = -1
        elif self._parts > other.partitions():
            p = 1
        else: p = 0
        #
        if self._dists < other.distinctions():
            d = -1
        elif self._dists > other.distinctions():
            d = 1
        else: d = 0
        # comparison vector
        return (n, p, d)
    
    def __eq__(self, other):
        if not isinstance(other, NameContext):
            return False
        return self.compare(other) == (0, 0, 0)
    
    def __ne__(self, other):
        if not isinstance(other, NameContext):
            return True
        return self.compare(other) != (0, 0, 0)
    
    def __gt__(self, other):
        if not isinstance(other, NameContext):
            return False
        return self.compare(other) > (0, 0, 0)

    def __ge__(self, other):
        if not isinstance(other, NameContext):
            return False
        return self.compare(other) >= (0, 0, 0)
    
    def __lt__(self, other):
        if not isinstance(other, NameContext):
            return False
        return self.compare(other) < (0, 0, 0)
    
    def __le__(self, other):
        if not isinstance(other, NameContext):
            return False
        return self.compare(other) <= (0, 0, 0)
    
    def __hash__(self):
        return hash((self._namenv, self._parts, self._dists))
    
    def __repr__(self):
        return "%r; %r; %r" %(self._namenv,self._parts,self._dists)
    
    
class ControlContext:
    """ A control context
    """
    def __init__(self, markings):
        self._markings = markings
    
    def marking(self, rname=None):
        if rname is None:
            return map(lambda x:x[1], self._markings)
        else:
            l = 0
            r = len(self._markings) - 1
            while l <= r:
                m = (l + r) / 2
                if self._markings[m][0] == rname:
                    return self._markings[m][1]
                elif rname < self._markings[m][0]:
                    r = m - 1
                else:
                    l = m + 1
                    
    def replace(self, rname, marking):
        p = self.pos(rname)
        M = self._markings
        M = M[:p] + ((rname, marking),) + M[p + 1:]
        return ControlContext(M)
                    
    def pos(self, rname):
        l = 0
        r = len(self._markings) - 1
        while l <= r:
            m = (l + r) / 2
            if self._markings[m][0] == rname:
                return m
            elif rname < self._markings[m][0]:
                r = m - 1
            else:
                l = m + 1

    def atomicRewrites(self, graph):
        """ Compute possible atomic transitions
        """
        rws = []
        for m in self.marking():
            rws.extend(m.atomicRewrites(graph))
        return rws
    
    def rewrite(self, rw):
        """ Update the thread distribution
        """
        if isinstance(rw, AtomicRewrite):
            if rw.isMono():
                return self
            elif rw.isSpwn():
                return self.rewriteSpwn(rw)
            elif rw.isTerm():
                return self.rewriteTerm(rw)
            else:  # norm
                return self.rewriteNorm(rw)
        else:  # sync
            rwo = rw.atomicOut()
            rwi = rw.atomicIn()
            if rwo.rname() != rwi.rname():
                return self.rewrite(rwo).rewrite(rwi)
            elif rwo.isMono() and rwi.isSpwn():
                rname = rwo.rname()
                m = self.marking(rname)
                i = m.generator().min()
                v1 = rwo.target()
                v2 = rwi.target()
                m = m.spawn(v1)
                m = m.spawn(v2)
                m = m.back(i, v1)
                return self.replace(rname, m)
            elif rwo.isTerm() and rwi.isSpwn():
                return self.rewrite(rwi).rewrite(rwo)
            else:
                return self.rewrite(rwo).rewrite(rwi)
    
    def rewriteSpwn(self, rw):
        """ Update thread distributor after spawning a thread
        """
        rname = rw.rname()
        target = rw.target()
        m = self.marking(rname)
        m = m.spawn(target)
        return self.replace(rname, m)
    
    def rewriteTerm(self, rw):
        """ Update thread distributor after terminating a thread
        """
        rname = rw.rname()
        thread = rw.thread()
        source = rw.source()
        m = self.marking(rname)
        m = m.back(thread, source)
        return self.replace(rname, m)
    
    def rewriteNorm(self, rw):
        """ Move a thread between two nodes
        """
        rname = rw.rname()
        thread = rw.thread()
        source = rw.source()
        target = rw.target()
        m = self.marking(rname)
        m = m.move(thread, source, target)
        return self.replace(rname, m)
    
    def __eq__(self, other):
        if not isinstance(other, ControlContext):
            return False
        return self.marking() == other.marking()
    
    def __ne__(self, other):
        if not isinstance(other, ControlContext):
            return True
        return self.marking() != other.marking()
    
    def __hash__(self):
        return hash(tuple(self.marking()))
    

class ReplicatorMarking:
    """ Thread distribution of a replicator.
    """
    def __init__(self, rname, generator, threads):
        self._rname = rname
        self._gen = generator
        self._threads = threads  # a TupleMap
        
    def rname(self):
        return self._rname
            
    def generator(self):
        return self._gen
    
    def threads(self):
        return self._threads
    
    def move(self, thread, source, target):
        """ Move thread between nodes
        """
        T1 = self.rm(thread, source)
        T2 = self.add(thread, target)
        M = self._threads.replace(source, T1).replace(target, T2)
        return ReplicatorMarking(self._rname, self._gen, M)
    
    def spawn(self, target):
        """ Move thread from the generator
        """
        thread, G = self._gen.take()
        T = self.add(thread, target)
        M = self._threads.replace(target, T)
        return ReplicatorMarking(self._rname, G, M)

    def back(self, thread, source):
        """ Move thread back to the generator
        """
        T = self.rm(thread, source)
        M = self._threads.replace(source, T)
        G = self._gen.put(thread)
        return ReplicatorMarking(self._rname, G, M)
    
    def add(self, thread, vertex):
        T = self._threads.val(vertex)
        if len(T) == 0:
            return (thread,)
        else:
            l = 0
            r = len(T) - 1
            while l <= r:
                m = (l + r) / 2
                if thread < T[m]:
                    r = m - 1
                else:
                    l = m + 1
            if T[m] < thread: m = m + 1
            return T[:m] + (thread,) + T[m:]
    
    def rm(self, thread, vertex):
        T = self._threads.val(vertex)
        l = 0
        r = len(T) - 1
        while l <= r:
            m = (l + r) / 2
            if T[m] == thread:
                break
            elif thread < T[m]:
                r = m - 1
            else:
                l = m + 1
        return T[:m] + T[m + 1:]
    
    def atomicRewrites(self, pi):
        """ Compute possible atomic rewrites
        """
        r = pi.replicator(self._rname)
        inodes = r.initialNodes()
        fnodes = r.finalNodes()
        rws = [] # rewrites
        if not self._gen.empty():
            i = self._gen.min()
            for target in inodes:
                stype = StrlType.SPWN
                if target in fnodes: 
                    stype = StrlType.MONO
                ga = r.node(target)
                rws.append(AtomicRewrite(self._rname, ga, i, None, target, stype))
        successors = r.succ()
        for src in successors:
            threads = self._threads.val(src)
            if len(threads) == 0: continue
            for target in successors[src]:
                ga = r.node(target)
                stype = StrlType.NORM
                if target in fnodes: 
                    stype = StrlType.TERM
                for i in threads:
                    rws.append(AtomicRewrite(self._rname, ga, i, src, target, stype))
        return rws
    
    def __eq__(self, other):
        if not isinstance(other, ReplicatorMarking):
            return False
        return (self._gen == other.generator() 
                and self._threads == other.threads())
        
    def __ne__(self, other):
        if not isinstance(other, ReplicatorMarking):
            return True
        return (self._gen != other.generator() 
                or self._threads != other.threads())
    
    def __hash__(self):  # TODO:
        return hash((self._gen, self._threads))


class ContextBuilder:
    """ A context builder of name/control context
    """
    def __init__(self):
        pass
    
    def buildNameContext(self, graph):
        """ Create a name context
        """
        E = self.createNameEnv(graph)
        P = self.createPartitions(E)
        D = self.createDistinctions(P)
        return NameContext(E, P, D)
    
    def buildControlContext(self, graph):
        """ Create a control context
        """
        M = []
        for r in graph.replicator():
            m = self.createMarking(r)
            M.append((r.name(), m))
        M.sort()
        return ControlContext(tuple(M))
    
    def build(self, graph):
        """ Create both name context and control context
        """
        return (self.buildNameContext(graph), self.buildControlContext(graph))
    
    def createNameEnv(self, graph):
        """ Create a name environment from a pi-graph
        """
        M = []
        k = 0
        for name in graph.gresNames():
            k = k + 1
            M.append((name, PrivateName(k)))
        for name in graph.freeNames():
            M.append((name, name))
        M.sort()
        return NameEnv(M)
    
    def createPartitions(self, name_env):
        """ Create a Partitions
        """
        M = []
        k = 0
        for name in name_env.cod():
            k = k + 1
            M.append((name, k))
        M.sort()
        return Partitions(M)
    
    def createDistinctions(self, partitions):
        """ Create a Distinctions based on a dynamic partitions
        """
        E = []
        names = []
        for name in partitions.dom():
            names.append(name)
        for i in range(len(names) - 1):
            for j in range(i + 1, len(names)):
                if not isinstance(names[i], FreeName) or not isinstance(names[j], FreeName):
                    p1 = partitions.val(names[i])
                    p2 = partitions.val(names[j])
                    if p1 > p2:
                        p1, p2 = p2, p1
                    E.append((p1, p2))
        E.sort()
        return Distinctions(E)
    
    def createMarking(self, r):
        """ Create a distributor for a replicator
        """
        gen = Generator(r.bound())
        nodes = r.node()
        nodes.sort()
        M = []
        for node in nodes:
            M.append((node, tuple()))
        return ReplicatorMarking(r.name(), gen, TupleMap(M))
    

class Interval(object):
    """ An interval
    """
    def __init__(self, lo, hi=None):
        self._lo = lo
        self._hi = hi

    def lo(self):
        return self._lo

    def hi(self):
        return self._hi

    def single(self):
        return self._lo == self._hi

    def sup(self):
        return self._hi is None
    
    def __contains__(self, n):
        return n >= self._lo and (self._hi is None or self._hi >= n)
    
    def __eq__(self, other):
        if not isinstance(other, Interval):
            return False
        return (self._lo, self._hi) == (other.lo(), other.hi())
    
    def __ne__(self, other):
        if not isinstance(other, Interval):
            return True
        return (self._lo, self._hi) != (other.lo(), other.hi())
    
    def __gt__(self, other):
        if not isinstance(other, Interval):
            return False
        return (self._lo, self._hi) > (other.lo(), other.hi())
    
    def __ge__(self, other):
        if not isinstance(other, Interval):
            return False
        return (self._lo, self._hi) >= (other.lo(), other.hi())

    def __lt__(self, other):
        if not isinstance(other, Interval):
            return False
        return (self._lo, self._hi) < (other.lo(), other.hi())

    def __le__(self, other):
        if not isinstance(other, Interval):
            return False
        return (self._lo, self._hi) <= (other.lo(), other.hi())

    def __str__(self):
        if self._lo == self._hi:
            return "%d" % self._lo
        elif self._hi is None:
            return "[%d..+inf]" % self._lo
        else:
            return "[%d..%d]" % (self._lo, self._hi)
    
    def __repr__(self):
        if self._lo == self._hi:
            return "%d" % self._lo
        elif self._hi is None:
            return "[%d..+inf]" % self._lo
        else:
            return "[%d..%d]" % (self._lo, self._hi)
    
    def __hash__(self):
        return hash((self._lo, self._hi))


class Generator():
    """ A thread generator
    """
    def __init__(self, bound=None, intervals=None):
        self._bound = bound
        if bound is None:
            self._intervals = (Interval(1),)
        elif intervals is None:
            self._intervals = (Interval(1, bound),)
        else:
            self._intervals = intervals
            
    def bound(self):
        return self._bound
    
    def empty(self):
        return len(self._intervals) == 0
    
    def take(self):
        """ Take the minimum thread
        """
        I0 = self._intervals[0]
        if I0.single():
            G = Generator(self._bound, self._intervals[1:])
            return I0.lo(), G
        else:
            k = I0.lo()
            I0 = Interval(I0.lo() + 1, I0.hi())
            G = Generator(self._bound, (I0,) + self._intervals[1:])
            return k, G
    
    def put(self, k):
        """ Put a thread back
        """
        if len(self._intervals) == 0:
            return Generator(self._bound, (Interval(k, k),))
        p = self.hole(k)
        if p == 0:
            if k != self._intervals[0].lo() - 1:
                return Generator(self._bound, (Interval(k, k),) + self._intervals)
            else:
                I = Interval(k, self._intervals[0].hi())
                return Generator(self._bound, (I,) + self._intervals[1:])
        elif p == len(self._intervals):
            if k != self._intervals[p - 1].hi() + 1:
                return Generator(self._bound, self._intervals + (Interval(k, k),))
            else:
                I = Interval(self._intervals[p - 1].lo(), k)
                return Generator(self._bound, self._intervals[:p - 1] + (I,))
        else:
            return self.insert(k, p)
        
    def insert(self, k, p):
        """ Insert a thread before an interval
        """
        I1 = self._intervals[p - 1]
        I2 = self._intervals[p]
        if I2.lo() - I1.hi() == 2:
            I = Interval(I1.lo(), I2.hi())
            return Generator(self._bound, self._intervals[:p - 1] + (I,) + self._intervals[p + 1:])
        elif k == I1.hi() + 1:
            I = Interval(I1.lo(), k)
            return Generator(self._bound, self._intervals[:p - 1] + (I,) + self._intervals[p:])
        elif k == I2.lo() - 1:
            I = Interval(k, I2.hi())
            return Generator(self._bound, self._intervals[:p] + (I,) + self._intervals[p + 1:])
        else:
            I = Interval(k, k)
            return Generator(self._bound, self._intervals[:p] + (I,) + self._intervals[p:])
    
    def hole(self, k):
        if len(self._intervals) == 0: return 0
        l = 0
        r = len(self._intervals) - 1
        while l <= r:
            m = (l + r) / 2
            if k < self._intervals[m].lo():
                if m == l or (l < m and self._intervals[m - 1].hi() < k):
                    return m
                else:
                    r = m
            else:
                if m == r or (m < r and k < self._intervals[m + 1].lo()):
                    return m + 1
                else:
                    l = m + 1
    
    def min(self, num=None):
        """ Test first/second minimum threads
        @param num: which value?
            1: the first minimum (or omitted)
            2: the second minimum
        """
        if num is None or num == 1:
            return self._intervals[0].lo()
        elif self._intervals[0].single():
            return self._intervals[1].lo()
        else:
            return self._intervals[0].lo() + 1
    
    def hastwo(self):
        """ Check if it can generate at least 2 threads.
        """
        if len(self._intervals) == 0:
            return False
        elif len(self._intervals) == 1:
            return not self._intervals[0].single()
        else: 
            return True
    
    def __contains__(self, k):
        l = 0
        r = len(self._intervals) - 1
        while l <= r:
            m = (l + r) / 2
            if k in self._intervals[m]:
                return True
            elif k < self._intervals[m].lo():
                r = m - 1
            else:
                l = m + 1
        return False
    
    def _comparable(self, other):
        if not isinstance(other, Generator):
            return False
        if self._bound != other.bound():
            return False
        else:
            return True

    def __eq__(self, other):
        if not self._comparable(other):
            return False
        return self._intervals == other._intervals
    
    def __ne__(self, other):
        if not self._comparable(other):
            return True
        return self._intervals != other._intervals
    
    def __gt__(self, other):
        if not self._comparable(other):
            return False
        return self._intervals > other._intervals
    
    def __ge__(self, other):
        if not self._comparable(other):
            return False
        return self._intervals >= other._intervals
    
    def __lt__(self, other):
        if not self._comparable(other):
            return False
        return self._intervals < other._intervals
    
    def __le__(self, other):
        if not self._comparable(other):
            return False
        return self._intervals <= other._intervals
    
    def __hash__(self):
        return hash((self._bound, self._intervals))
    
    def __str__(self):
        return ", ".join(str(inter) for inter in self._intervals)

    def __repr__(self):
        return ", ".join(repr(inter) for inter in self._intervals)
    
        
class PiContext(object):
    """ A state of pi-graph
    """
    def __init__(self, nc, cc):
        self._nc = nc
        self._cc = cc
        
    def nameContext(self):
        """ Get the name context.
        """
        return self._nc
    
    def ctrlContext(self):
        """ Get the control context.
        """
        return self._cc
    
    def activate(self, trans, grp):
        """ Activate a transition
        """
        nc, cc = trans.post(self._nc, self._cc, grp)
        nc = nc.normalize()
        return PiContext(nc, cc)
    
    def __hash__(self):
        return hash((self._nc, self._cc))
    
    def __eq__(self, other):
        ''' Check if two states are equal.'''
        if not isinstance(other, PiContext):
            raise False
        if hash(self) != hash(other):
            return False
        return (self._nc == other.nameContext() and 
                self._cc == other.ctrlContext())
    
    def __ne__(self, other):
        ''' Check if two states are not equal.'''
        if not isinstance(other, PiContext):
            return False
        return hash(self) != hash(other)
    
 
class PiContextGraph(object):
    """ A state graph of pi-graph
    """
    def __init__(self, grp):
        self._gr = grp
        self._hash_table = {}  # hash --> list of state objects
        self._ID_state = {}  # <hash, displace> --> integer (state value)
        self._state_ID = {}  # integer --> <hash, displace>
        self._todo = []  # queue of state numbers
        self._succ = {}
        self._pred = {}
        self._last = -1
        self._built = False

        bld = ContextBuilder()
        nc, cc = bld.build(self._gr)
        stateObj_0 = PiContext(nc, cc)  # initial state object
        hash_value = hash(stateObj_0)
        self._createState(stateObj_0, hash_value)
        
    def build(self, stop=None):
        """ Build a state graph.
        @param stop: maximum number of states
        @return: True if build successfully, and number of generated states
        """
        self._built = True
        while (len(self._todo) > 0) and (stop is None or self._todo[0] <= stop):
            state = self._todo.pop(0)
            self._process(state)
        return self._last + 1
    
    def isCompleted(self):
        """ Test if the state graph is complete
        """
        if not self._built:
            raise Exception("must build first")
        return len(self._todo) == 0
    
    def numOfStates(self):
        if not self._built:
            raise Exception("must build first")
        return self._last + 1
    
    def getState(self, state=None):
        if state is None:
            return self._state_ID.keys()
        else:
            object_ID = self._state_ID[state]
            hash_value = object_ID[0]  # first component is hash value
            displace = object_ID[1]  # second component is displace
            return self._hash_table[hash_value][displace]
            
    def getSuccessors(self, state):
        """ Get next states
        """
        return self._succ[state].keys()
    
    def getPredecessors(self, state):
        """ Get previous states
        """
        return self._pred[state].keys()
    
    def getActions(self, source, target):
        """ Get all actions
        @param source: the source state
        @param target: the new state
        """
        return self._succ[source][target]
    
    def _process(self, state):
        state_obj = self.getState(state)
        transitions = self.computeAllRewrites(state_obj)
        if len(transitions) == 0:
            return
        for trans in transitions:
            if trans.pre(state_obj.nameContext(), self._gr):
                next_state_obj = state_obj.activate(trans, self._gr)
                hash_value = hash(next_state_obj)
                target = None
                if self._isNewState(next_state_obj, hash_value):
                    target = self._createState(next_state_obj, hash_value)
                else:
                    target = self._getStateID(next_state_obj, hash_value)
                self._createEdge(state, target, trans)
    
    def computeSyncs(self, IOs, nc, cc):
        """ Compute possible synchronizations
        @param IOs: list of input, output
        @param nc: name context
        @param cc: control context
        """
        syncs = []
        L = len(IOs)
        for i in range(L - 1):
            for j in range(i + 1, L):
                t1 = IOs[i]
                t2 = IOs[j]
                if t1.action().__class__ == t2.action().__class__: 
                    continue
                if t1.rname() == t2.rname():
                    if t1.source() == t2.source() == None:  # spawn 2 threads
                        gen = cc.marking(t1.rname()).generator()
                        if not gen.hastwo():
                            continue
                        i2 = gen.min(2)
                        if isinstance(t1.action(), Input):
                            t1 = t1.changeThread(i2)
                        else:
                            t2 = t2.changeThread(i2)
                    elif t1.source() == t2.source() and t1.thread() == t2.thread():
                        continue  # !!! important
                if isinstance(t1.action(), Output):
                    syncs.append(SyncRewrite(t1, t2))
                else:
                    syncs.append(SyncRewrite(t2, t1))
        return syncs

    def computeAllRewrites(self, state):
        """ Compute possible transitions (atomic transitions and sync).
        """
        # categorize transitions
        nc = state.nameContext()
        cc = state.ctrlContext()
        atomics = cc.atomicRewrites(self._gr)
        taus = []
        pubIOs = []
        prvIOs = []
        for t in atomics:
            if isinstance(t.action(), Silence):
                taus.append(t)
            elif t.priv(nc,self._gr):
                prvIOs.append(t)
            else:
                pubIOs.append(t)
        pubSyncs = self.computeSyncs(pubIOs, nc, cc)
        prvSyncs = self.computeSyncs(prvIOs, nc, cc)
        return (taus + pubIOs + pubSyncs + prvSyncs)
    
    def _isNewState(self, state_obj, hash_value):
        """ Test if a state is a new one
        """
        if hash_value not in self._hash_table.keys():
            return True
        for obj in self._hash_table[hash_value]:
            if obj == state_obj:  # very important!
                return False
        return True

    def _createState(self, state_obj, hash_value):
        """ Create a new state
        """
        ID = tuple([hash_value, 0])
        if hash_value in self._hash_table.keys():
            self._hash_table[hash_value].append(state_obj)
            displace = len(self._hash_table[hash_value]) - 1
            ID = tuple([hash_value, displace])
        else:  # create new item in the hash table
            self._hash_table[hash_value] = [state_obj]
        
        self._last += 1
        self._ID_state[ID] = self._last
        self._state_ID[self._last] = ID
        
        self._pred[self._last] = {}
        self._succ[self._last] = {}
        self._todo.append(self._last)
        return self._last
        
    def _getStateID(self, state_obj, hash_value):
        """ Get state number of a state object
        """
        objs = self._hash_table[hash_value]
        displace = 0
        for i in range(len(objs)):
            if objs[i] == state_obj:
                displace = i
                break
        return self._ID_state[tuple([hash_value, displace])]
    
    def _createEdge (self, source, target, action):
        """ Create a connection between states
        """
        if target in self._succ[source]:
            self._succ[source][target].add(action)
        else:
            self._succ[source][target] = set([action])
        if source in self._pred[target]:
            self._pred[target][source].add(action)
        else:
            self._pred[target][source] = set([action])